/************************************************************************
 * TestEngine/Examples - Automata Identification Engine
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     
 * Description  :     
 * Change log   :     	-Date:  Change
 ************************************************************************/
﻿using System;
using System.Collections.Generic;
using MBT.Modeling;
using SMLib.DataTypes;
using CoreDES.Utils;

namespace TestingApp.Examples
{
	public class TFTP_Model
	{
		public TFTP_Model ()
		{
			ackedPack = -1;
			mainReqSent = false;
			req = "";
			RightFile = false;
		}

		/// <summary>
		/// If the main request (put or get) is sent or not
		/// </summary>
		public bool mainReqSent;
		public bool RightFile;
		public int ackedPack;
		/// <summary>
		/// Last request by client
		/// </summary>
		public string req;
		#region [Get]
		[ActionAttrib.Exec("Get", ActionType.controllable)]
		public void Get ()
		{
			int s = Choice.Some<int> (1, 2);
			//* get the right file
			if (s == 1) {
				req = "Get 1";
				RightFile = true;
			}
            //* get the wrong file
            else {
				req = "Get 2";
				RightFile = false;
			}

			ackedPack = 0;
			mainReqSent = true;
		}

		[ActionAttrib.Pre("Get")]
		public bool Get_Enabled ()
		{
			//* it will be enabled just if it was not sent the main request before
			return (!mainReqSent && req == "");
		}
		#endregion
		#region [ack]
		[ActionAttrib.Exec("Ack", ActionType.controllable)]
		public void Ack ()
		{
			int s = Choice.Some<int> (0, 1);
			if (s == 1)
				ackedPack = 1;
			req = "Ack " + s;
		}

		[ActionAttrib.Pre("Ack")]
		public bool Ack_Enabled ()
		{
			return req == "";
		}
		#endregion
		#region [data]
		[ActionAttrib.Exec("Data", ActionType.observable)]
		public void Data ()
		{
			req = "";
		}

		[ActionAttrib.Pre("Data")]
		public bool Data_Enabled ()
		{
			return (req == "Get 1"
                ||
				(req == "Ack 0" && ackedPack == 0 && mainReqSent && RightFile));
		}
		#endregion
		#region [err]
		[ActionAttrib.Exec("Err", ActionType.observable)]
		public void Err ()
		{
			req = "";
		}

		[ActionAttrib.Pre("Err")]
		public bool Err_Enabled ()
		{
			return (
			//* get a wrong file
                req == "Get 2" ||
			//* send an ack without a request
				((req == "Ack 0" || req == "Ack 1") && !mainReqSent));
		}
		#endregion
		#region [to]
		[ActionAttrib.Exec("TO", ActionType.observable)]
		public void TO ()
		{
			req = "";
		}

		[ActionAttrib.Pre("TO")]
		public bool TO_Enabled ()
		{
			return (req == "Ack 0" || req == "Ack 1") && ackedPack == 1 && mainReqSent;
		}
		#endregion
		/// <summary>
		/// Factory method
		/// </summary>
		public static object[] Construct ()
		{
			TFTP_Model c = new TFTP_Model ();
			return new object[] { c };
		}
	}
}
